$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$;${\it da}$).
\\[0ex]ecl{-}trans{-}a($A$)
\\[0ex]$\in$ $\mathbb{N}\rightarrow$($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ecl{-}trans{-}ks($A$)) \}$\rightarrow$State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$ecl{-}trans{-}type($A$)$\rightarrow\mathbb{B}$)